Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    f(g(x),g(y))  → f(p(f(g(x),s(y))),g(s(p(x))))
2:    p(0)  → g(0)
3:    g(s(p(x)))  → p(x)
There are 6 dependency pairs:
4:    F(g(x),g(y))  → F(p(f(g(x),s(y))),g(s(p(x))))
5:    F(g(x),g(y))  → P(f(g(x),s(y)))
6:    F(g(x),g(y))  → F(g(x),s(y))
7:    F(g(x),g(y))  → G(s(p(x)))
8:    F(g(x),g(y))  → P(x)
9:    P(0)  → G(0)
The approximated dependency graph contains one SCC: {4}.
Tyrolean Termination Tool  (0.05 seconds)   ---  May 3, 2006